$\forall$$A$:Type, $l$:($A$ List). ge($\parallel$$l$$\parallel$; 1) $\Rightarrow$ (hd($l$) $\in$ $A$)